Analyses of unsatisfiability for equational logic programming
Identifieur interne : 00C649 ( Main/Exploration ); précédent : 00C648; suivant : 00C650Analyses of unsatisfiability for equational logic programming
Auteurs : Maria Alpuente [Espagne] ; Moreno Falaschi [Espagne] ; Ferdinando Manzo [Espagne]Source :
- The Journal of Logic Programming [ 0743-1066 ] ; 1995.
English descriptors
- Teeft :
- Abstract interpretation, Abstract semantics, Abstract state, Abstract state domain, Abstract states, Abstract substitutions, Abstract term, Abstract transition system, Algorithm, Alpuente, Approximation relation, Calculus, Canonical, Computer science, Conditional, Conditional term, Conf, Constraint, Derivation, Eager normalization, Eager normalization analysis, Equation description, Equation sets, Equational, Equational logic, Equational logic programming, Equational logic programs, Equational theories, Equational theory, Equivalence classes, Execution state, Existentially, Falaschi, Finite number, Finite sets, Function symbol, Function symbols, Functional dependencies, General unifier, Ground instances, Horn equational, Horn equational theories, Horn equational theory, Ieee, Incremental, Initial state, Irreducible, Joinability, Lecture notes, Logic programming, Loop check, Node, Nonunifiability, Nonunifiability analysis, Normal forms, Normalization, Operational semantics, Other methods, Proc, Programming, Programming languages, Reduction rule, Reduction rules, Search tree, Semantics, Simple technique, State description, Substitution, Substitution description, Technical report, Theoretical computer science, Transition system, Transition systems, Unification algorithm, Unification rule, Unifier, Unquantified, Unsatisfiability, Unsatisfiable.
Abstract
Abstract: The problem of unifying pairs of terms with respect to an equational theory (as well as detecting the unsatisfiability of a system of equations) is, in general, undecidable. In this work, we define a framework based on abstract interpretation for the (static) analysis of the unsatisfiability of equation sets. The main idea behind the method is to abstract the process of semantic unification of equation sets based on narrowing. The method consists of building an abstract narrower for equational theories, and executing the sets of equations to be detected for unsatisfiability in the approximated narrower. As an instance of our framework, we define a new analysis whose accuracy is enhanced by some simple loop-checking technique. This analysis can also be actively used for pruning the search tree of an incremental equational constraint solver, and can be integrated with other methods in the literature. Standard methods are shown to be an instance of our framework. To the best of our knowledge, this is the first framework proposed for approximating equational unification.
Url:
DOI: 10.1016/0743-1066(94)00024-Z
Affiliations:
Links toward previous steps (curation, corpus...)
- to stream Istex, to step Corpus: 001F44
- to stream Istex, to step Curation: 001F19
- to stream Istex, to step Checkpoint: 002A64
- to stream Main, to step Merge: 00CF06
- to stream Main, to step Curation: 00C649
Le document en format XML
<record><TEI wicri:istexFullTextTei="biblStruct"><teiHeader><fileDesc><titleStmt><title>Analyses of unsatisfiability for equational logic programming</title><author><name sortKey="Alpuente, Maria" sort="Alpuente, Maria" uniqKey="Alpuente M" first="Maria" last="Alpuente">Maria Alpuente</name></author><author><name sortKey="Falaschi, Moreno" sort="Falaschi, Moreno" uniqKey="Falaschi M" first="Moreno" last="Falaschi">Moreno Falaschi</name></author><author><name sortKey="Manzo, Ferdinando" sort="Manzo, Ferdinando" uniqKey="Manzo F" first="Ferdinando" last="Manzo">Ferdinando Manzo</name></author></titleStmt><publicationStmt><idno type="wicri:source">ISTEX</idno><idno type="RBID">ISTEX:87CF402BFF901ACAC68C47DA8141A7B7FBDC0A83</idno><date when="1995" year="1995">1995</date><idno type="doi">10.1016/0743-1066(94)00024-Z</idno><idno type="url">https://api.istex.fr/ark:/67375/6H6-P65L6GS7-7/fulltext.pdf</idno><idno type="wicri:Area/Istex/Corpus">001F44</idno><idno type="wicri:explorRef" wicri:stream="Istex" wicri:step="Corpus" wicri:corpus="ISTEX">001F44</idno><idno type="wicri:Area/Istex/Curation">001F19</idno><idno type="wicri:Area/Istex/Checkpoint">002A64</idno><idno type="wicri:explorRef" wicri:stream="Istex" wicri:step="Checkpoint">002A64</idno><idno type="wicri:doubleKey">0743-1066:1995:Alpuente M:analyses:of:unsatisfiability</idno><idno type="wicri:Area/Main/Merge">00CF06</idno><idno type="wicri:Area/Main/Curation">00C649</idno><idno type="wicri:Area/Main/Exploration">00C649</idno></publicationStmt><sourceDesc><biblStruct><analytic><title level="a">Analyses of unsatisfiability for equational logic programming</title><author><name sortKey="Alpuente, Maria" sort="Alpuente, Maria" uniqKey="Alpuente M" first="Maria" last="Alpuente">Maria Alpuente</name><affiliation wicri:level="1"><country wicri:rule="url">Espagne</country></affiliation><affiliation wicri:level="2"><country xml:lang="fr">Espagne</country><wicri:regionArea>Departamento de Sistemas Informáticos y Computación, Universidad Politécnica de Valencia, Camino de Vera s/n, Apdo. 22012, 46020 Valencia</wicri:regionArea><placeName><region nuts="2" type="communauté">Communauté valencienne</region></placeName></affiliation></author><author><name sortKey="Falaschi, Moreno" sort="Falaschi, Moreno" uniqKey="Falaschi M" first="Moreno" last="Falaschi">Moreno Falaschi</name><affiliation wicri:level="2"><country xml:lang="fr">Espagne</country><wicri:regionArea>Departamento de Sistemas Informáticos y Computación, Universidad Politécnica de Valencia, Camino de Vera s/n, Apdo. 22012, 46020 Valencia</wicri:regionArea><placeName><region nuts="2" type="communauté">Communauté valencienne</region></placeName></affiliation></author><author><name sortKey="Manzo, Ferdinando" sort="Manzo, Ferdinando" uniqKey="Manzo F" first="Ferdinando" last="Manzo">Ferdinando Manzo</name><affiliation wicri:level="2"><country xml:lang="fr">Espagne</country><wicri:regionArea>Departamento de Sistemas Informáticos y Computación, Universidad Politécnica de Valencia, Camino de Vera s/n, Apdo. 22012, 46020 Valencia</wicri:regionArea><placeName><region nuts="2" type="communauté">Communauté valencienne</region></placeName></affiliation></author></analytic><monogr></monogr><series><title level="j">The Journal of Logic Programming</title><title level="j" type="abbrev">JLP</title><idno type="ISSN">0743-1066</idno><imprint><publisher>ELSEVIER</publisher><date type="published" when="1995">1995</date><biblScope unit="volume">22</biblScope><biblScope unit="issue">3</biblScope><biblScope unit="page" from="223">223</biblScope><biblScope unit="page" to="254">254</biblScope></imprint><idno type="ISSN">0743-1066</idno></series></biblStruct></sourceDesc><seriesStmt><idno type="ISSN">0743-1066</idno></seriesStmt></fileDesc><profileDesc><textClass><keywords scheme="Teeft" xml:lang="en"><term>Abstract interpretation</term><term>Abstract semantics</term><term>Abstract state</term><term>Abstract state domain</term><term>Abstract states</term><term>Abstract substitutions</term><term>Abstract term</term><term>Abstract transition system</term><term>Algorithm</term><term>Alpuente</term><term>Approximation relation</term><term>Calculus</term><term>Canonical</term><term>Computer science</term><term>Conditional</term><term>Conditional term</term><term>Conf</term><term>Constraint</term><term>Derivation</term><term>Eager normalization</term><term>Eager normalization analysis</term><term>Equation description</term><term>Equation sets</term><term>Equational</term><term>Equational logic</term><term>Equational logic programming</term><term>Equational logic programs</term><term>Equational theories</term><term>Equational theory</term><term>Equivalence classes</term><term>Execution state</term><term>Existentially</term><term>Falaschi</term><term>Finite number</term><term>Finite sets</term><term>Function symbol</term><term>Function symbols</term><term>Functional dependencies</term><term>General unifier</term><term>Ground instances</term><term>Horn equational</term><term>Horn equational theories</term><term>Horn equational theory</term><term>Ieee</term><term>Incremental</term><term>Initial state</term><term>Irreducible</term><term>Joinability</term><term>Lecture notes</term><term>Logic programming</term><term>Loop check</term><term>Node</term><term>Nonunifiability</term><term>Nonunifiability analysis</term><term>Normal forms</term><term>Normalization</term><term>Operational semantics</term><term>Other methods</term><term>Proc</term><term>Programming</term><term>Programming languages</term><term>Reduction rule</term><term>Reduction rules</term><term>Search tree</term><term>Semantics</term><term>Simple technique</term><term>State description</term><term>Substitution</term><term>Substitution description</term><term>Technical report</term><term>Theoretical computer science</term><term>Transition system</term><term>Transition systems</term><term>Unification algorithm</term><term>Unification rule</term><term>Unifier</term><term>Unquantified</term><term>Unsatisfiability</term><term>Unsatisfiable</term></keywords></textClass><langUsage><language ident="en">en</language></langUsage></profileDesc></teiHeader><front><div type="abstract" xml:lang="en">Abstract: The problem of unifying pairs of terms with respect to an equational theory (as well as detecting the unsatisfiability of a system of equations) is, in general, undecidable. In this work, we define a framework based on abstract interpretation for the (static) analysis of the unsatisfiability of equation sets. The main idea behind the method is to abstract the process of semantic unification of equation sets based on narrowing. The method consists of building an abstract narrower for equational theories, and executing the sets of equations to be detected for unsatisfiability in the approximated narrower. As an instance of our framework, we define a new analysis whose accuracy is enhanced by some simple loop-checking technique. This analysis can also be actively used for pruning the search tree of an incremental equational constraint solver, and can be integrated with other methods in the literature. Standard methods are shown to be an instance of our framework. To the best of our knowledge, this is the first framework proposed for approximating equational unification.</div></front></TEI><affiliations><list><country><li>Espagne</li></country><region><li>Communauté valencienne</li></region></list><tree><country name="Espagne"><noRegion><name sortKey="Alpuente, Maria" sort="Alpuente, Maria" uniqKey="Alpuente M" first="Maria" last="Alpuente">Maria Alpuente</name></noRegion><name sortKey="Alpuente, Maria" sort="Alpuente, Maria" uniqKey="Alpuente M" first="Maria" last="Alpuente">Maria Alpuente</name><name sortKey="Falaschi, Moreno" sort="Falaschi, Moreno" uniqKey="Falaschi M" first="Moreno" last="Falaschi">Moreno Falaschi</name><name sortKey="Manzo, Ferdinando" sort="Manzo, Ferdinando" uniqKey="Manzo F" first="Ferdinando" last="Manzo">Ferdinando Manzo</name></country></tree></affiliations></record>Pour manipuler ce document sous Unix (Dilib)
EXPLOR_STEP=$WICRI_ROOT/Wicri/Lorraine/explor/InforLorV4/Data/Main/Exploration
HfdSelect -h $EXPLOR_STEP/biblio.hfd -nk 00C649 | SxmlIndent | more
Ou
HfdSelect -h $EXPLOR_AREA/Data/Main/Exploration/biblio.hfd -nk 00C649 | SxmlIndent | more
Pour mettre un lien sur cette page dans le réseau Wicri
{{Explor lien
|wiki= Wicri/Lorraine
|area= InforLorV4
|flux= Main
|étape= Exploration
|type= RBID
|clé= ISTEX:87CF402BFF901ACAC68C47DA8141A7B7FBDC0A83
|texte= Analyses of unsatisfiability for equational logic programming
}}
| This area was generated with Dilib version V0.6.33. |  |